// DATA TYPE

sig Txt{}
sig Time{
			hour : Int,
			minute : Int
}
sig Date{}
sig Bool{}

// ENTITIES DEFINITION

sig Event{
			event_id: Int,
			place: Txt,
			title: Txt,
			time1: Time,
			time2: Time,
			date1: Date,
			date2: Date,
			type_io: Bool,
			type_pp: Bool,
			description: Txt,
			isOrganized: one User,
}


sig Invitation{
			answer: Bool,
			relativeTo: one Event,
			sentTo: one User
}

sig Weather{
			weather_id: Int,
			description: Txt,
			image: Txt,
}

sig User{
			nickname: Txt,
			name: Txt,
			surname: Txt,
			mail: Txt,
			password: Txt,
			public_cal: Bool
}

sig Forecast{
			forecast_id: Int,
			date: Date,
			place: Txt,
			relatedTo: one Weather
}

// FACT

//two users for the same event
fact differentUser{
			no disj u,u': User,e:Event | e.isOrganized = u and e.isOrganized =u'
}

// two users haven't the same nickname
fact differentNickname{
			no disj u, u' : User | u.nickname = u'.nickname or u.mail = u'.mail
}

// two events haven't the same id
fact differentEventId{
			no disj e, e' : Event | e.event_id = e'.event_id
}

// two forecast haven't the same id
fact differentForecastId{
			no disj f, f' : Forecast | f.forecast_id = f'.forecast_id
}

// two weather haven't the same id
fact differentWeathertId{
			no disj w, w' : Weather | w.weather_id = w'.weather_id
}

// an event with the same date and the feasible time
fact sameDateFeasibleTime{
			all e: Event | e.date1 = e.date2 implies e.time2.hour >= e.time1.hour
}

// an user can't invite himself
fact userAutoInvite{
			all i:Invitation, e:Event, u:User |  e.isOrganized = u implies( i.sentTo != u)
}

// every forecast is related to an event 
fact forecastEvent{
			all e:Event| some f:Forecast | e.date1 = f.date and e.place = f.place
}

// two invitations to the same user
fact userInvitation{
			no disj i,i':Invitation| i.relativeTo = i'.relativeTo and i.sentTo = i'.sentTo
} 

//PREDICATES

pred show(){}
run show for 3

// user organize event
pred organizeNewEvent(u : User,e', e : Event){
		e.isOrganized = e'.isOrganized + u
		
}
run organizeNewEvent

// add user
pred addUser(u:User, nm,n,s,e,p:Txt,b:Bool){
		u.name = nm
		u.nickname = n
		u.surname = s
		u.mail = e
		u.password = p
		u.public_cal = b
		all e:Event, i:Invitation| e.isOrganized != u and i.sentTo != u 
}
run addUser

// add invitation
pred addInvitation(e: Event, i:Invitation, u:User, b:Bool){
			i.sentTo = u and
			i.relativeTo = e	 and
			i.answer = b
}
run addInvitation

// ASSERTIONS

// any new user has a unique mail and nickname
assert nicknameMail{
			all disj u,u':User, nm,n,s,e,p:Txt,b:Bool | addUser[u, nm,n,s,e,p,b] implies
			(u.nickname != u'.nickname and u.mail != u'.mail)
}
check nicknameMail

// two invitation can't be sent at the same user from the same event
assert uniqueInvitation{
			no disj i,i': Invitation| all u:User, e:Event, b:Bool | addInvitation[e, i, u, b] implies
			(i.relativeTo = i'.relativeTo and i.sentTo = i'.sentTo)
}
check uniqueInvitation
